package gov.nasa.jpf.symbc.probsym;

import org.apache.bcel.classfile.JavaClass;
import org.apache.bcel.util.Repository;
import org.apache.bcel.util.SyntheticRepository;

import gov.nasa.jpf.*;
import gov.nasa.jpf.symbc.mutation.Mutater;
import gov.nasa.jpf.symbc.mutation.MutationListener;

public class JPFJavaMutate {

	private static Mutater mutater = new Mutater(-1);

	private static int mutationCount = 0;

	private static MutationListener mutationListener = null;

	private static void prepareMutater(Config conf, String[] restricted) {
		// Prepare for mutations
		Repository repository = SyntheticRepository.getInstance();
		mutater.setRepository(repository);
		for (String r : restricted) {
			mutater.addRestrictedMethod(r);
		}
		try {
			String target = conf.getString("target");
			JavaClass targetClass = repository.loadClass(target);
			if (targetClass != null) {
				mutationCount = mutater.countMutationPoints(target);
				mutationListener = new MutationListener(target, mutater,
						targetClass);
			} else {
				mutationCount = 0;
			}
		} catch (ClassNotFoundException e) {
			mutationCount = 0;
		}
		// mutationCount = 1;
	}

	private static void setCommonConfig(Config conf, String... restricted) {
		conf.setProperty("classpath", "${jpf-symbc}/build/examples;${jpf-symbc}/build/main");
		conf.setProperty("sourcepath", "${jpf-symbc}/src/examples");
		conf.setProperty("symbolic.solver.slicing", "true");
		conf.setProperty("symbolic.solver.canonization", "true");
		conf.setProperty("symbolic.solver.dp", "cvc3");
		conf.setProperty("symbolic.solver.mc", "latte");
//		conf.setProperty("symbolic.solver.mc.tool", "lib/count.osx");
		conf.setProperty("symbolic.solver.mc.tool", "/home/jaco/latte-integrale-1.5.3/latte-int-1.5/code/latte/count");
		conf.setProperty("symbolic.solver.store", "redis");
//		conf.setProperty("symbolic.solver.store.redis.delay", "true");
//		conf.setProperty("symbolic.solver.store", "redislevel");
//		conf.setProperty("symbolic.solver.store.redislevel.host", "localhost,41.215.236.166");
//		conf.setProperty("symbolic.solver.store.redislevel.host", "localhost,146.232.212.14");
		conf.setProperty("symbolic.prob_modelcounter", ".symbc.modelcounter.latte.LattECounter");
		conf.setProperty("listener", ".symbc.SymbolicListenerSuperClean");
//		conf.setProperty("listener", ".symbc.probsym.ProbSymListener");
//		conf.setProperty("listener", ".symbc.SymStatsListener");
		conf.setProperty("vm.storage.class", "nil");
		prepareMutater(conf, restricted);
	}

	private static void setBinomialHeapBugConfig(Config conf) {
		conf.setProperty("target", "probsym.BinomialHeapBug");
		conf.setProperty("symbolic.method", "probsym.BinomialHeapBug.runTestDriver(con);");
		conf.setProperty("symbolic.min_int", "0");
		conf.setProperty("symbolic.max_int", "9");
		for (int i = 0; i < 10; i++) {
			conf.setProperty("symbolic.min_int_c" + i, "1");
			conf.setProperty("symbolic.max_int_c" + i, "2");
		}
		setCommonConfig(conf, "merge");
	}

	private static void setBinomialHeapConfig(Config conf) {
		conf.setProperty("target", "probsym.BinomialHeap");
		conf.setProperty("symbolic.method", "probsym.BinomialHeap.runTestDriver(con);");
		conf.setProperty("symbolic.min_int", "0");
		conf.setProperty("symbolic.max_int", "9");
		for (int i = 0; i < 10; i++) {
			conf.setProperty("symbolic.min_int_c" + i, "1");
			conf.setProperty("symbolic.max_int_c" + i, "2");
		}
		setCommonConfig(conf, "merge");
	}

	private static void setTreeMapConfig(Config conf) {
		conf.setProperty("target", "probsym.TreeMap");
		conf.setProperty("symbolic.method", "probsym.TreeMap.runTestDriver(con);");
		conf.setProperty("symbolic.min_int", "0");
		conf.setProperty("symbolic.max_int", "9");
		for (int i = 0; i < 10; i++) {
			conf.setProperty("symbolic.min_int_c" + i, "1");
			conf.setProperty("symbolic.max_int_c" + i, "2");
		}
		setCommonConfig(conf, "containsKey", "getEntry", "put", "remove", "successor", "rotateRight");
	}

	private static void setBinTreeConfig(Config conf) {
		conf.setProperty("target", "probsym.BinTree");
		conf.setProperty("symbolic.method", "probsym.BinTree.runTestDriver(con);");
		conf.setProperty("symbolic.min_int", "0");
		conf.setProperty("symbolic.max_int", "9");
		for (int i = 0; i < 8; i++) {
			conf.setProperty("symbolic.min_int_c" + i, "1");
			conf.setProperty("symbolic.max_int_c" + i, "2");
		}
		setCommonConfig(conf, "delete", "insert", "getSuccessor");
	}

	private static void setTritypConfig(Config conf) {
		conf.setProperty("target", "probsym.Trityp");
		conf.setProperty("symbolic.method", "probsym.Trityp.classify(sym#sym#sym);");
		conf.setProperty("symbolic.min_int", "0");
		conf.setProperty("symbolic.max_int", "1073741824");
		setCommonConfig(conf, "classify");
	}

	private static void setMutationTestProgramConfig(Config conf) {
		conf.setProperty("target", "probsym.MutationTestProgram");
		conf.setProperty("symbolic.method", "probsym.MutationTestProgram.test(sym);");
//		conf.setProperty("symbolic.method", "probsym.MutationTestProgram.testSilly(sym);");
		conf.setProperty("symbolic.min_int", "0");
		conf.setProperty("symbolic.max_int", "9");
		setCommonConfig(conf, "test");
//		setCommonConfig(conf, "testSilly");
	}

	private static long runMutation(Config conf, int mutation) {
		mutater.setMutationPoint(mutation);
		System.out.println("######################################################################");
		System.out.println("#");
		System.out.println("# Running mutation " + (mutation + 1) + " of " + mutationCount);
		System.out.println("#");
		System.out.println("######################################################################");
		long elapsedTime = System.currentTimeMillis();
		try {
			JPF jpf = new JPF(conf);
			jpf.addListener(mutationListener);
			jpf.run();
			elapsedTime = System.currentTimeMillis() - elapsedTime;
			System.out.println("#");
			System.out.println("# Mutation was: "
					+ mutationListener.getModification());
			System.out.println("# Elapsed time (msec) : " + elapsedTime);
			System.out.println("#");
			if (jpf.foundErrors()) {
				// ... process property violations discovered by JPF
			}
		} catch (JPFConfigException cx) {
			// ... handle configuration exception
			cx.printStackTrace();
		} catch (JPFException jx) {
			// ... handle exception while executing JPF
			jx.printStackTrace();
		}
		return elapsedTime;
	}

	/**
	 * @param args
	 */
	public static void main(String[] args) {
		Config conf = new Config(args);
//		setBinomialHeapConfig(conf);
//		setBinomialHeapBugConfig(conf);
//		setTreeMapConfig(conf);
		setTritypConfig(conf);
//		setBinTreeConfig(conf);
//		setMutationTestProgramConfig(conf);

		long elapsedTime = 0;
		for (int m = -1; m < mutationCount; m++) {
			elapsedTime += runMutation(conf, m);
		}
		System.out.println("######################################################################");
		System.out.println("#");
		System.out.println("# Mutations done");
		System.out.println("# Total elapsed time (msec) : " + elapsedTime);
		System.out.println("#");
		System.out.println("######################################################################");
	}

}
